;;;
;;; wff.lisp: Syntax of First-Order Logic
;;;
;;; By Philip W. L. Fong
;;;
;;; Defines the syntax of first-order terms and formulas (page 1-2, 
;;; lecture 18).  Also provides facilities for performing substitutions 
;;; in a first-order formula (page 2, lecture 20).
;;;
;;; Example:  The formula on page 7, lecture 20 is represented as
;;;           follows:
;;;
;;;  (forall ?x (and (p ?x ?x)
;;;                  (exists ?y (=> (forall ?x (p ?x ?y))
;;;                                 (p ?x ?y)))))
;;;

;; Terms: constructors, selectors and recognizers

;; Variables

;; A variable is a symbol with its name beginning with '?'
;; e.g. '?a, '?this-is-a-variable, '?123

(defun make-fresh-variable ()
  "Generate a fresh variable that is guaranteed to be different from
any existing variables."
  (let ((v (gentemp "?")))
    v))

(defun variable-p (term)
  (and (symbolp term)
       (eql #\? (char (symbol-name term) 0))))

;; Constants

;; A constant is a non-variable symbol.
;; e.g. 'a, 'this-is-a-constant

(defun constant-p (term)
  (and (symbolp term)
       (not (eql #\? (char (symbol-name term) 0)))))


;; Function applications

(defun make-funapp (symbol term-list)
  (cons symbol term-list))

(defun funapp-symbol (funapp)
  (first funapp))

(defun funapp-term-list (funapp)
  (rest funapp))

(defun funapp-p (term)
  (consp term))

;; WFF's: constructors, selectors and recognizers

;; Atomic formulas

(defun make-atom (predicate-sym term-list)
  (cons predicate-sym term-list))

(defun atom-predicate-sym (atom)
  (first atom))

(defun atom-term-list (atom)
  (rest atom))

(defun atom-p (wff)
  (not (member (first wff) '(not or and => <=> forall exists))))

;; Negations

(defun make-negation (wff)
  (list 'not wff))

(defun negation-wff (negation)
  (second negation))

(defun negation-p (wff)
  (eq (first wff) 'not))

;; Disjunctions

(defun make-disjunction (wff1 wff2)
  (list 'or wff1 wff2))

(defun disjunction-wff1 (disjunction)
  (second disjunction))

(defun disjunction-wff2 (disjunction)
  (third disjunction))

(defun disjunction-p (wff)
  (eq (first wff) 'or))

;; Conjunctions

(defun make-conjunction (wff1 wff2)
  (list 'and wff1 wff2))

(defun conjunction-wff1 (conjunction)
  (second conjunction))

(defun conjunction-wff2 (conjunction)
  (third conjunction))

(defun conjunction-p (wff)
  (eq (first wff) 'and))

;; Implications

(defun make-implication (wff1 wff2)
  (list '=> wff1 wff2))

(defun implication-wff1 (implication)
  (second implication))

(defun implication-wff2 (implication)
  (third implication))

(defun implication-p (wff)
  (eq (first wff) '=>))

;; Equivalences

(defun make-equivalence (wff1 wff2)
  (list '<=> wff1 wff2))

(defun equivalence-wff1 (equivalence)
  (second equivalence))

(defun equivalence-wff2 (equivalence)
  (third equivalence))

(defun equivalence-p (wff)
  (eq (first wff) '<=>))

;; Universally quantified formulas

(defun make-universal (var wff)
  (list 'forall var wff))

(defun universal-var (universal)
  (second universal))

(defun universal-wff (universal)
  (third universal))

(defun universal-p (wff)
  (eq (first wff) 'forall))

;; Existentially quantified formulas

(defun make-existential (var wff)
  (list 'exists var wff))

(defun existential-var (existential)
  (second existential))

(defun existential-wff (existential)
  (third existential))

(defun existential-p (wff)
  (eq (first wff) 'exists))

;;
;; Substitution mechanism for WFF and terms.
;; An implementation of the algorithm specified in page 2 of lecture 20.
;;

(defun wff-substitute (wff var value)
  "Substitue a term VALUE for a free variable VAR in a formula WFF."
  (cond
   ((negation-p wff) 
    (make-negation (wff-substitute (negation-wff wff) var value)))
   ((disjunction-p wff)
    (make-disjunction (wff-substitute (disjunction-wff1 wff) var value)
		      (wff-substitute (disjunction-wff2 wff) var value)))
   ((conjunction-p wff)
    (make-conjunction (wff-substitute (conjunction-wff1 wff) var value)
		      (wff-substitute (conjunction-wff2 wff) var value)))
   ((implication-p wff)
    (make-implication (wff-substitute (implication-wff1 wff) var value)
		      (wff-substitute (implication-wff2 wff) var value)))
   ((equivalence-p wff)
   (make-equivalence (wff-substitute (equivalence-wff1 wff) var value)
		      (wff-substitute (equivalence-wff2 wff) var value)))
   ((universal-p wff)
    (if (eq (universal-var wff) var)
	wff
      (make-universal (universal-var wff)
		      (wff-substitute (universal-wff wff) var value))))
   ((existential-p wff)
    (if (eq (existential-var wff) var)
	wff
      (make-existential (existential-var wff)
			(wff-substitute (existential-wff wff) var value))))
   (t (atom-substitute wff var value))))

(defun atom-substitute (atom var value)
  "Substitute a term VALUE for free variable VAR in an atomic formula ATOM."
  (make-atom (atom-predicate-sym atom)
	     (mapcar #'(lambda (x) (term-substitute x var value))
		     (atom-term-list atom))))

(defun term-substitute (term var value)
  "Substituting a term VALUE for free variable VAR in a term TERM."
  (cond
   ((constant-p term) term)
   ((variable-p term) 
    (if (eq term var)
	value
      term))
   (t
    (make-funapp (funapp-symbol term) 
		 (mapcar #'(lambda (x) (term-substitute x var value))
			 (funapp-term-list term))))))


